T:Type, eq:EqDecider(T), a, b:(T List).
l_disjoint(T;a;b)  (l_intersection(eq;a;b) = []  (T List)) 

latex

Definitions	(x  l), x:A  B(x), P & Q, Void, x:AB(x), P  Q, False, A, x:A. B(x), t  T, , type List, s = t, P  Q, P  Q, EqDecider(T), Type, l_disjoint(T;l1;l2), l_intersection(eq;L1;L2), b, hd(l), i <z j, i z j, l[i], A  B, a < b, , #$n, ||as||, n+m, i  j , i  j < k, {x:A| B(x)} , {i..j},
Lemmas	nil member, member-intersection, select member, le wf, non neg length, length wf1, not wf, l member wf